es:ES, e:E. (isrcv(e))  (destination(lnk(e)) = loc(e)  Id) 

latex

Definitions	P  Q, x:A. B(x), isrcv(e), t  T, b, loc(e), destination(l), <a, b>, Id, s = t, E, P & Q, x:AB(x), ES
Lemmas	es-axioms, assert wf, es-isrcv wf